Nuprl Lemma : append-cancellation 0,22

T:Type, asas'bscs:T List.
||as|| = ||as'||    (as @ cs) = (as' @ bs T List  cs = bs 
latex


DefinitionsP & Q, t  T, x:AB(x), ||as||, P  Q, {T}, P  Q, Prop, as @ bs
Lemmasappend wf, general-append-cancellation, length wf1

origin